from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
FROM(X) → FROM(s(X))
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
FROM(X) → FROM(s(X))
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
LENGTH(cons(X, Y)) → LENGTH1(Y)
LENGTH1(X) → LENGTH(X)
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LENGTH(cons(X, Y)) → LENGTH1(Y)
Used ordering: Polynomial interpretation [25,35]:
LENGTH1(X) → LENGTH(X)
The value of delta used in the strict ordering is 1/8.
POL(LENGTH(x1)) = 1/4 + (1/4)x_1
POL(cons(x1, x2)) = 1/2 + (2)x_2
POL(LENGTH1(x1)) = 1/4 + (1/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
LENGTH1(X) → LENGTH(X)
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
FROM(X) → FROM(s(X))
from(X) → cons(X, from(s(X)))
length(nil) → 0
length(cons(X, Y)) → s(length1(Y))
length1(X) → length(X)